 \begin{module}{\moduleName{IMP-SEMANTICS}}
 \including{\moduleName{IMP-SYNTAX}\modulePlus{}\moduleName{K}}
 \begin{latexComment}
\subsection*{Semantics}
 This module defines the semantics of IMP.  We first define
 its configuration, then its results, and then its semantic rules. 
 \end{latexComment}
 \begin{latexComment}
 \subsection*{Configuration}
 The configuration of IMP is trivial: it only contains two cells, one for
 for the computation and another for the state.  For good encapsulation
 and clarity, we place the two cells inside another cell, the ``top'' cell. 
 \end{latexComment}
 \kconfig{\kallLarge{yellow}{T}{\kallLarge{green}{k}{\dotCt{K}}\mathrel{}\kallLarge{red}{state}{\dotCt{Map}}}}
 \begin{latexComment}
  \subsection{Results}
 IMP only has two types of results: integers and Booleans. 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{KResult}}}{\crlbracket{\nonTerminal{\sort{Bool}}}}{}
 \syntaxCont{\nonTerminal{\sort{KResult}}}{\crlbracket{\nonTerminal{\sort{Int}}}}{}
 \begin{latexComment}
  \subsection{Arithmetic Expressions}
 The \K semantics of each arithmetic construct is defined below.
 We need to do nothing for integers. 
 \end{latexComment}
 \begin{latexComment}
  \subsubsection{Variable Lookup}
 A program variable $X$ is looked up in state $\Large\sigma$ using the
 builtin map lookup operation ${\Large\sigma}(X)$.  Note that this
 operation requires $\Large\sigma$ to be defined in $X$; otherwise the
 rewriting process will get stuck.  This means that our semantics of
 IMP disallows uses of uninitialized variables. 
 \end{latexComment}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{\variable{X}{Id}}{{{\variable{\displayGreek{\sigma}}{Map}}\mathrel{\terminal{(}}{\variable{X}{Id}}\mathrel{\terminal{)}}}}}}\mathrel{\terminal{}}{\kall{red}{state}{\variable{\displayGreek{\sigma}}{Map}}}}}
 \begin{latexComment}
  \subsubsection{Arithmetic operators}
 There is nothing special about these, except that the rule for division
 has a side condition. 
 \end{latexComment}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{+}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}
 \kcrule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{/}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\ensuremath{{}\div}\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}{\ensuremath{{\variable{\ensuremath{{I}_{2}}}{Int}}\mathrel{\terminal{$\neq$\subscript{{\scriptstyle\it{}Bool}}}}{\constant{0}{Zero}}}}
 \begin{latexComment}
  \subsection{Boolean Expressions}
 The rules below are straightforward.  Note the short-circuited semantics
 of \textsf{and}; this is the reason we annotated the syntax of
 \textsf{and} with the \K attribute "strict(1)" instead of "strict". 
 \end{latexComment}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{<=}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\ensuremath{\leq}\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}
 \krule{}{\ensuremath \reduceTop{{\terminal{not}{\variable{T}{Bool}}}}{{\mathrel{\terminal{$\neg$\subscript{{\scriptstyle\it{}Bool}}}}{\variable{T}{Bool}}}}}
 \krule{}{\ensuremath \reduceTop{{{\constant{true}{Bool}}\terminal{and}{\variable{B}{BExp}}}}{\variable{B}{BExp}}}
 \krule{}{\ensuremath \reduceTop{{{\constant{false}{Bool}}\terminal{and}{\AnyVar{List\{K\}}}}}{\constant{false}{Bool}}}
 \subsection{Statements}
 There is one rule per statement construct except for the conditional,
 which needs two rules. 
 \begin{latexComment}
  \subsubsection{Skip}
 The \texttt{skip} statement is simply dissolved.  One can make this
 rule structural if one does not want it to count as a computational step. 
 \end{latexComment}
 \krule{}{\ensuremath \reduceTop{\constant{\ensuremath{\terminal{skip;}}}{Stmt}}{\dotCt{K}}}
 \begin{latexComment}
  \subsubsection{Assignment}
 The assigned variable is updated in the state: ${\Large\sigma}[I/X]$
 adds the mapping $X \mapsto I$ to $\Large\sigma$ in case $\Large\sigma$
 is not defined in $X$, and it changes the current mapping of $X$
 (to point to $I$) in case $\Large\sigma$ is defined in $X$.
 At the same time, the assignment is dissolved. 
 \end{latexComment}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{{{\variable{X}{Id}}\terminal{=}{\variable{I}{Int}}\terminal{;}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{red}{state}{\reduce{\variable{\displayGreek{\sigma}}{Map}}{{{\variable{\displayGreek{\sigma}}{Map}}\mathrel{\terminal{[}}{\variable{I}{Int}}\mathrel{\terminal{/}}{\variable{X}{Id}}\mathrel{\terminal{]}}}}}}}}
 \begin{latexComment}
  \subsubsection{Sequential Composition}
 Sequential composition is simply dissolved into the \K's builtin
 task sequentialization operation.  Like for \texttt{skip}, one is
 free to make this rule structural if one does not want it to count
 as a computational step.  
 \end{latexComment}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{S}_{1}}}{Stmt}}\mathrel{}{\variable{\ensuremath{{S}_{2}}}{Stmt}}}}{{{\variable{\ensuremath{{S}_{1}}}{Stmt}}\mathrel{\terminal{\ensuremath{\kra}}}{\variable{\ensuremath{{S}_{2}}}{Stmt}}}}}
 \begin{latexComment}
  \subsubsection{Conditional}
 The conditional statement has two semantic cases, corresponding to
 when its condition evaluates to \texttt{true} or to \texttt{false}. 
 \end{latexComment}
 \krule{}{\ensuremath \reduceTop{{\terminal{if}{\constant{true}{Bool}}\terminal{then}{\variable{S}{Stmt}}\terminal{else}{\AnyVar{List\{K\}}}}}{\variable{S}{Stmt}}}
 \krule{}{\ensuremath \reduceTop{{\terminal{if}{\constant{false}{Bool}}\terminal{then}{\AnyVar{List\{K\}}}\terminal{else}{\variable{S}{Stmt}}}}{\variable{S}{Stmt}}}
 \begin{latexComment}
  \subsubsection{While Loop}
 We give the semantics of the \texttt{while} loop by unrolling.
 Note that the unrolling takes place only when the loop statement
 reaches the top of the computation cell; otherwise the unrolling
 process may not terminate.  Recall that \K is a rewriting
 framework, so one needs to structurally (or via strategies, which
 \K does not support for model-theoretical reasons) inhibit the
 application of rewrite rules; this is in contrast to SOS, where one
 needs to explicitly give permission (through conditional rules) to
 reductions inside constructs' arguments.  Also note that we prefered
 to make the rule below structural.  If one wants this unrolling step
 to count as a computational step (though we beg one to reconsider)
 then one can remove the ``structural'' tag.  
 \end{latexComment}
 \kequation{}{\ensuremath \kprefix{green}{k}{\reduceS{{\terminal{while}{\variable{B}{BExp}}\terminal{do}{\variable{S}{Stmt}}}}{{\terminal{if}{\variable{B}{BExp}}\terminal{then}{{{\variable{S}{Stmt}}\mathrel{}{{\terminal{while}{\variable{B}{BExp}}\terminal{do}{\variable{S}{Stmt}}}}}}\terminal{else}{\constant{\ensuremath{\terminal{skip;}}}{Stmt}}}}}}
 \end{module}
 \begin{module}{\moduleName{IMP}}
 \including{\moduleName{K}}
 \including{\moduleName{IMP-PROGRAMS}\modulePlus{}\moduleName{IMP-SEMANTICS}}
 \syntax{\nonTerminal{\sort{Bag}}}{\llbracket\,{\nonTerminal{\sort{KLabel}}}\,\rrbracket}{}
 \mequation{}{{\llbracket\,{\variable{KL}{KLabel}}\,\rrbracket}}{\kmiddle{yellow}{T}{\kall{green}{k}{{{\variable{KL}{KLabel}}\mathrel{\terminal{(}}{\constant{\ensuremath{\dotCt{List\{K\}}}}{List\{KResult\}}}\mathrel{\terminal{)}}}}}}
 \end{module}